es:ES.
es-Send(es)
 i:Idk:Kndkindcase(k; a.es-V(es)(i,a); l,t.es-M(es)(l,t) )state@i(Msg(es-M(es)) List) 

latex

Definitions	t  T, es-T(es), vartype(i;x), es-Send(es), es-M(es), state@i, es-V(es), x:A  B(x), ES, x:AB(x), Id, Knd, Type, f(a), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, x:A. B(x)
Lemmas	event system wf